Modern verification tools use a variety of individual engines based on different algorithms, such as binary decision diagram (BDD) based reachability, propositional or Boolean satisfiability (SAT) based bounded model checking (BMC), interpolations, and property-directed reachability (PDR), to name a few. These engines may have drastically different performances on different problems. Given a design configured as a finite-state machine (FSM), these verification engines check to see whether a certain state can be reached from the initial states. The individual verification engines thus can either prove the property that the improper state cannot be reached, or falsify the property with a trace connecting a valid initial state to the improper state. Verification engines that are primarily designed to prove that an improper state cannot be reached may be referred to as “prove” engines, while verification engines that are primarily designed to trace an initial state to a bad state may be referred to as “falsify” engines.
For a verification problem, the task of engine orchestration is to select and schedule the appropriate engines to run the problem. Engine orchestration is a very challenging problem and may help determine the overall performance of a verification suite. Traditionally, ad-hoc heuristics, combined with trial-and-error, have been used to orchestrate the various engines. This may not be very effective, with success often determined by the experience level of the test engineer, luck, or other variables.
One seminal difficulty in orchestrating a variety of engines based on different solvers and algorithms, each with unique characteristics and capacities, is the lack of a “best” algorithm—an algorithm superior to all others in all, or even most, design test cases. Even a generally slow engine can sometimes be exponentially faster than a generally fast engine, depending on the specific details of a verification problem. More importantly, some engines are designed to falsify a problem, and do not have the ability to prove a problem, while other engines are designed to prove a problem and may be poor at falsification. Today, engines are typically scheduled in a static order, and most, if not all, current orchestration techniques assume that a given verification engine has an equal chance of successfully proving or falsifying any given design.